COMMENT ⊗   VALID 00201 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00011 00002	/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=BAXS30/FONT#4=GACS25/FONT#5=CLAR30/FONT#8=SAIL25
C00012 00003
C00013 00004
C00016 00005	↓ ↓N↓α↓ ε↑↓ b1
C00017 00006	often
C00018 00007	researchα
C00019 00008	AIα
C00020 00009	alsoα
C00021 00010	applications     ↓ π∞↓exempli↓↓↓βC↓↓↓edα
C00022 00011	howα
C00023 00012	thisαworkα
C00024 00013	↓↓↓βC↓↓↓tsα
C00025 00014	together.α
C00026 00015	 Ourαlong
C00027 00016	goalα
C00028 00017	isα
C00029 00018	aαprogramα
C00030 00019	thatα
C00031 00020	canα
C00032 00021	beα
C00033 00022	toldαfacts
C00035 00023	 Sometimesαitα
C00036 00024	willαuseα
C00037 00025	theseα
C00038 00026	factsαto
C00039 00027	"expertα
C00040 00028	programs"α
C00041 00029	thatα
C00042 00030	useα
C00043 00031	theseα
C00044 00032	facts
C00045 00033	aα
C00046 00034	moreαe↓↓↓β@↓↓↓icientα
C00047 00035	wayα
C00048 00036	thanα
C00049 00037	simpleαreasoning.
C00050 00038	producingα
C00051 00039	programs"α
C00052 00040	new      ↓ π∞↓Weα↔doα↔notα↔proposeα↔toα↔implementα↔suchαa
C00053 00041	 Theα
C00054 00042	increasingα
C00055 00043	emphasisα
C00056 00044	ARPA        ↓ π∞↓programα→immediatelyα→-α→maybeα→notα→atα→all
C00057 00045	agenciesα
C00058 00046	AIα
C00059 00047	on      ↓ π∞↓withinα
C00060 00048	theα
C00061 00049	nextα
C00062 00050	↓↓↓βC↓↓↓veα
C00063 00051	years.α
C00064 00052	 Thisα
C00065 00053	isα
C00066 00054	becauseαits
C00067 00055	onα
C00068 00056	of
C00069 00057	exclusivelyα
C00070 00058	forseeable
C00071 00059	 Inα
C00072 00060	weα
C00073 00061	willα
C00074 00062	theoretical
C00076 00063	areαavailableαforα
C00077 00064	solvingαa    ↓ π∞↓1.α∂Developmentα∂ofα∂↓↓circumscription↓α∂asα∂aα∂mode
C00078 00065	concernsα
C00079 00066	proceduresα
C00080 00067	forα
C00081 00068	decidingα
C00082 00069	to     ↓ π∞↓processα
C00083 00070	ofα
C00084 00071	concludingα(oftenα
C00085 00072	incorrectly)α
C00086 00073	thatαa
C00087 00074	↓ ↓N↓α↓ ε↑↓ `2
C00088 00075	formalαsystemα
C00089 00076	thatαaα
C00090 00077	candidateαproofα
C00091 00078	canαbe
C00093 00079	ofα
C00094 00080	modern
C00095 00081	eventsα
C00096 00082	place.      ↓ π∞↓checkersα⊂forα⊂theα⊂formalα⊂systemsα⊂inα⊂logicα∂and
C00097 00083	theoryα
C00098 00084	textbooks,α
C00099 00085	andαweα
C00100 00086	didα
C00101 00087	itα
C00102 00088	someαyears
C00103 00089	proofs,αandαtheα
C00104 00090	excessαin
C00106 00091	actuallyαisα
C00107 00092	metamathematicalαreasoning
C00108 00093	he
C00109 00094	shortcutsα
C00110 00095	whoseα
C00111 00096	repeatedα
C00112 00097	keeps
C00114 00098	↓ ↓N↓α↓ ε↑↓ `3
C00115 00099	largeαcollectionαofα
C00116 00100	proofsαto
C00117 00101	asα
C00118 00102	toα
C00119 00103	ideas
C00121 00104	didn'tα
C00122 00105	knowα
C00123 00106	theαcolorsα
C00124 00107	ofα
C00125 00108	theirα
C00126 00109	ownαspots
C00127 00110	problemα
C00128 00111	non-
C00129 00112	whatα
C00130 00113	to
C00132 00114	reasoningα
C00133 00115	mustα
C00134 00116	beα
C00135 00117	ableα
C00136 00118	toαprove      ↓ π∞↓McCarthy-Painterα↔compilerα↔(McCarthyα↔and
C00139 00119	inαprogress)α
C00140 00120	hasαusedα
C00141 00121	FOLαto
C00142 00122	ofα
C00143 00123	aα
C00144 00124	hardα
C00145 00125	retrospectiveα
C00146 00126	chessαproblem
C00147 00127	↓ ↓N↓α↓ ε↑↓ ]4
C00148 00128	buildα
C00149 00129	ofα
C00150 00130	world.      ↓ π∞↓LISPα
C00151 00131	proveα
C00152 00132	LISP
C00153 00133	B"α
C00154 00134	byα
C00155 00135	lookingαatα
C00156 00136	theα
C00157 00137	modelα
C00158 00138	ratherαthan        ↓ π∞↓inductionα↔intoα↓↓↓βC↓↓↓rstα↔orderαlogic.α↔ Thisαalso
C00159 00139	of      ↓ π∞↓requiresα∨theα∨metamathematicalα≡machinery.
C00160 00140	andα
C00161 00141	theα
C00162 00142	chess      ↓ π∞↓Weα∞expectα∞thisα∞toα∞beα∞su↓↓↓β@↓↓↓icientlyα∞practicalα∞for
C00163 00143	overα
C00164 00144	traditionalα
C00165 00145	formalizations.α
C00166 00146	 Filman's
C00167 00147	humansα
C00168 00148	observation       ↓ π∞↓programs.α_ Theseα_includeα_thingsα→likeα_how
C00169 00149	mathematical
C00170 00150	containα
C00171 00151	asα
C00172 00152	andα
C00173 00153	talk
C00174 00154	↓↓↓βC↓↓↓rstα
C00175 00155	theoremsα
C00176 00156	461     ↓ π∞↓haveα
C00177 00157	thatαitαtakesαoneα
C00178 00158	stepαjust    ↓ π∞↓computedα~byα~programs,α~notα≠propertiesα~of
C00179 00159	Weyhrauchα(Aiello
C00180 00160	systemαandαweα
C00181 00161	haveαjust
C00182 00162	weα
C00183 00163	aα
C00184 00164	of         ↓ π∞↓properties of certain related programs.
C00185 00165	isα
C00186 00166	trueα
C00187 00167	ifα
C00188 00168	theα
C00189 00169	S-expressionsα
C00190 00170	↓↓x↓   ↓ π∞↓(3)α→Theα→veri↓↓↓βC↓↓↓cationα→ofα→theα→correctnessα_of
C00192 00171	Theαveri↓↓↓βC↓↓↓cationα
C00193 00172	ofαtheα
C00194 00173	correctnessα
C00195 00174	ofαLISP     ↓ π∞↓hardwareα∩correctnessα∩areα∩oftenα∩simplerα∩than
C00196 00175	 Johnα
C00197 00176	McCarthyα
C00198 00177	1977d)       ↓ π∞↓proofsα⊃ofα⊃programα⊃correctness,α⊃becauseα⊃often
C00199 00178	↓ ↓N↓α↓ ε↑↓ ←5
C00200 00179	beenαaddedα
C00201 00180	toαFOL.α
C00202 00181	 Theseαinclude        ↓ π∞↓interest,α⊃andα∩weα⊃proposeα⊃aα∩rotatingα⊃research
C00204 00182	sentencesαofα
C00205 00183	theαmetamathematics,  ↓ π∞↓LaboratoryαisαdirectedαbyαJohnαMcCarthyαand
C00207 00184	eachαto
C00208 00185	remoteα
C00209 00186	toα
C00210 00187	computerα
C00211 00188	the
C00214 00189	andα
C00215 00190	pursueα
C00216 00191	thesisα
C00217 00192	researchαin    ↓ π∞↓American Mathematical Society,
C00219 00193	haveαexcitedα
C00220 00194	muchαoutside     ↓ π∞↓↓ πNComputing Machinery (1971).
C00221 00195	↓ ↓N↓α↓ ε↑↓ `6
C00229 00196	↓ ↓N↓α↓ ε↑↓ `7
C00236 00197	↓ ↓N↓α↓ ε↑↓ ←8
C00238 00198	↓ ↓N↓α↓ ε↑↓ `9
C00242 00199	↓ ↓N↓α↓ ε↑↓ P10
C00245 00200	↓ ↓N↓α↓ ε↑↓ V11
C00251 00201	
C00252 ENDMK
C⊗;
/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=BAXS30/FONT#4=GACS25/FONT#5=CLAR30/FONT#8=SAIL25



↓ ↓N↓↓ ¬∞Research Proposal Submitted to


↓ ↓N↓↓ ∧-↓αTHE NATIONAL SCIENCE FOUNDATION


↓ ↓N↓α↓ εK↓for


↓ ↓N↓↓ ∧R↓αBasic Research in Arti↓↓βc↓↓αcial Intelligence


↓ ↓N↓α↓ εN↓by


↓ ↓N↓↓ ¬wJohn McCarthy
↓ ↓N↓↓ ¬↔Professor of Computer Science
↓ ↓N↓↓ ¬QPrincipal Investigator








↓ ↓N↓↓ ¬wSeptember 1977





↓ ↓N↓↓ ¬→Computer Science Department

↓ ↓N↓↓ ¬ ↓αSTANFORD UNIVERSITY

↓ ↓N↓α↓ ¬[↓Stanford, California



↓ ↓N↓¬↓ ↓YResearch Proposal Submitted to the National Science Foundation





↓ ↓N↓Proposed Amount ↓&↓λ$423,225↓↓)αβ. Proposed E↓λ↓β@↓λ↓ective Date ↓&↓λ1 Jan. 1978↓↓)αβ. Proposed Duration ↓&↓λ3 years↓↓)αβ.



↓ ↓N↓Title ↓&↓λBasic Research in Artificial Intelligence↓↓)αβ



↓ ↓N↓Principal Investigator ↓&↓λJohn McCarthy↓↓)αβ↓ ε>Submitting Institution ↓&↓λStanford University↓↓)αβ
↓ ↓N↓  Soc. Sec. No. ↓&↓λ558-30-4793↓↓)αβ↓ ε>Department ↓&↓λ Computer Science    ↓↓)αβ
↓ ↓N↓↓ ε>Address ↓&↓λStanford, California 94305↓↓)αβ



↓ ↓N↓Make grant to ↓&↓λBoard of Trustees of the Leland Stanford Junior University↓↓)αβ



↓ ↓N↓Endorsements:

↓ ↓N↓↓ α↑Principal Investigator↓ ¬nDepartment Head↓ λnInstitutional Admin. O↓λ↓β@↓λ↓icial

↓ ↓N↓Name↓ α↑↓&↓λJohn McCarthy        ↓↓)αβ↓ ¬n↓&↓λEdward A. Feigenbaum ↓↓)αβ↓ λ}↓&↓λ                     ↓↓)αβ


↓ ↓N↓Signature↓ α↑↓&↓λ                     ↓↓)αβ↓ ¬n↓&↓λ                     ↓↓)αβ↓ λ}↓&↓λ                     ↓↓)αβ

↓ ↓N↓Title↓ α↑↓&↓λProfessor            ↓↓)αβ↓ ¬n↓&↓λProfessor & Chairman ↓↓)αβ↓ λ}↓&↓λ                     ↓↓)αβ

↓ ↓N↓Telephone↓ α↑↓&↓λ(415) 497-4430       ↓↓)αβ↓ ¬n↓&↓λ(415) 497-4079       ↓↓)αβ↓ λ}↓&↓λ                     ↓↓)αβ

↓ ↓N↓Date↓ α↑↓&↓λ                     ↓↓)αβ↓ ¬n↓&↓λ                     ↓↓)αβ↓ λ}↓&↓λ                     ↓↓)αβ
↓ ↓N↓α↓ ε↑↓ b1


↓ ↓N↓α↓ βEAbstract                                    ↓ π∞↓beenα∂chosenα∂thatα∂areα∂capableα∂ofα∂representing
                                            ↓ π∞↓onlyα∞aα
partα∞ofα
theα∞informationα
thatα∞wouldα
be
↓ ↓N↓Thisα⊃isα⊂aα⊃requestα⊂forα⊃aα⊂grantα⊃inα⊃supportα⊂of          ↓ π∞↓availableα∨toα∨aα∨human.α∨ Theα∨modesα≡of
↓ ↓N↓basicα⊗researchα∃inα⊗arti↓βC↓cialα⊗intelligenceα∃with    ↓ π∞↓reasoningα
usedα
byα
presentα
programsα
areα
often
↓ ↓N↓emphasisαonαtheαstructureαofαformalα
reasoning,    ↓ π∞↓evenα*weakerα)thanα*theα)representations
↓ ↓N↓epistemologicalα8problemsα8ofα8arti↓βC↓cial          ↓ π∞↓themselves.
↓ ↓N↓intelligenceα≠andα≠computerα≤proofα≠checking.
↓ ↓N↓Theα∃computerα∃proofα∃checkingα∃supportsα∀the         ↓ π∞↓Theα∂linesα∂ofα⊂researchα∂weα∂planα∂toα⊂pursueα∂are
↓ ↓N↓basicα
researchα
inα
AIα
butα
alsoα
hasα
applications     ↓ π∞↓exempli↓↓↓βC↓↓↓edα
inα
theα
enclosedα
papersα
(McCarthy
↓ ↓N↓toα-verifyingα,computerα-programsα,and              ↓ π∞↓1977a,b,c,d,α≠Mooreα≤1977).α≠ Hereα≤weα≠shall
↓ ↓N↓eventuallyα⊃toα∩checkingα⊃proofsα∩resultingα⊃from     ↓ π∞↓explainα
howα
thisαworkα
↓↓↓βC↓↓↓tsα
together.α
 Ourαlong
↓ ↓N↓research in mathematics.                    ↓ π∞↓rangeα
goalα
isα
aαprogramα
thatα
canα
beα
toldαfacts
                                            ↓ π∞↓aboutα∞theα∞worldα∞andα∞canα∞useα∞themα∞e↓↓↓β@↓↓↓ectively
↓ ↓N↓α↓ ↓{Epistemological Problems of Arti↓↓βc↓↓αcial       ↓ π∞↓toα
achieveα
theα
goalsα
itα
isα
given.α∞ Sometimesα
it
↓ ↓N↓ β/↓αIntelligence                                ↓ π∞↓willα⊂useα⊂theα⊂factsα∂directlyα⊂fromα⊂itsα⊂dataα∂base
                                            ↓ π∞↓usingα⊃deductiveα⊃andα⊃inductiveα⊃processesα⊃like
↓ ↓N↓Arti↓βC↓cialα→intelligenceα→hasα_provedα→toα→beα_a         ↓ π∞↓theα
deductiveα∞processesα
ofα∞mathematicalα
logic.
↓ ↓N↓di↓β@↓icultα≠branchα≤ofα≠science.α≤ Someα≠people         ↓ π∞↓However,α_weα_areα_alreadyα_sure,α↔(McCarthy
↓ ↓N↓thoughtα
thatα
human-levelα
intelligenceα
couldα
be   ↓ π∞↓1977a),α≠thatα≠conjecturalα≠processesα≠willα≠be
↓ ↓N↓achievedα∞inα∞tenα∞orα∞twentyα∞years,α∞butα∞thisα
was       ↓ π∞↓neededα
thatα
goα
beyondα
deductionα
asα
presently
↓ ↓N↓basedα∂onα∞theα∂di↓β@↓icultiesα∞theyα∂couldα∂seeα∞when       ↓ π∞↓conceived.α
 Sometimesαitα
willαuseα
theseα
factsαto
↓ ↓N↓theyα⊗madeα⊗theα⊗optimisticα⊗predictions.α∃ Our       ↓ π∞↓compileα
"expertα
programs"α
thatα
useα
theseα
facts
↓ ↓N↓ownα
opinionαisα
thatα
majorαscienti↓βC↓cα
discoveries   ↓ π∞↓inα
aα
moreαe↓↓↓β@↓↓↓icientα
wayα
thanα
simpleαreasoning.
↓ ↓N↓remainα≡toα≡beα≡madeα≡beforeα≡human-level             ↓ π∞↓However,α∪theα∩expertα∪programsα∩willα∪haveα∩to
↓ ↓N↓generalα~intelligenceα~isα~reached.α~ Moreover,     ↓ π∞↓deferα
toαreasoningα
whenαunexpectedα
useαofα
the
↓ ↓N↓manyα⊃ofα⊂theseα⊃discoveriesα⊃requireα⊂theoretical    ↓ π∞↓factual data-base is required.
↓ ↓N↓advancesα∀andα∪notα∀merelyα∀extendingα∪current
↓ ↓N↓ideasα
forα
producingα
"expertα
programs"α
toα
new      ↓ π∞↓Weα↔doα↔notα↔proposeα↔toα↔implementα↔suchα⊗a
↓ ↓N↓domains.α
 Theα
increasingα
emphasisα
byα
ARPA        ↓ π∞↓programα→immediatelyα→-α→maybeα→notα→atα→all
↓ ↓N↓andα
otherα
agenciesα
sponsoringα
AIα
researchα
on      ↓ π∞↓withinα
theα
nextα
↓↓↓βC↓↓↓veα
years.α
 Thisα
isα
becauseαits
↓ ↓N↓immediateα≠applicationsα≠hasα≠resultedα≤inα≠a         ↓ π∞↓successα
dependsα
onα
successfulα
formalizationα
of
↓ ↓N↓seriousα∩imbalance.α∪ Decidingα∩whatα∪theα∩basic      ↓ π∞↓factsα≥aboutα≥theα≤world.α≥ Weα≥haveα≤made
↓ ↓N↓issuesα⊂areα∂isα⊂di↓β@↓icultα∂enoughα⊂withoutα∂having      ↓ π∞↓progressα
inα
thisα
formalization,α
butα
weα
mayα
be
↓ ↓N↓toα(formulateα)everythingα(inα)termsα(of              ↓ π∞↓occupiedα
withα
itα
exclusivelyα
forα
theα
forseeable
↓ ↓N↓demonstrationα
programsαtoα
beα
availableαinα
two     ↓ π∞↓future.α
 Inα
shortα
weα
willα
emphasizeα
theoretical
↓ ↓N↓years.                                      ↓ π∞↓arti↓↓↓βC↓↓↓cialα∞intelligenceα
exceptα∞forα
theα∞workα
with
                                            ↓ π∞↓proof-checkers to be described below.
↓ ↓N↓Ourα⊃researchα⊂isα⊃basedα⊃onα⊂theα⊃ideaα⊃that,α⊂for
↓ ↓N↓manyα~purposes,α≠theα~problemsα≠ofα~arti↓βC↓cial         ↓ π∞↓Theα0mainα1areasα0ofα1ourα0previous
↓ ↓N↓intelligenceα∞canα∞beα
separatedα∞intoα∞twoα∞partsα
-     ↓ π∞↓accomplishmentα~andα≠futureα~workα≠areα~the
↓ ↓N↓anα⊂epistemologicalα⊂partα⊂andα⊂aα⊃heuristicα⊂part.     ↓ π∞↓following (as now seen):
↓ ↓N↓Theα⊃↓↓epistemological↓α⊂partα⊃concernsα⊃whatα⊂facts
↓ ↓N↓andαinferenceαrulesα
areαavailableαforα
solvingαa    ↓ π∞↓1.α∂Developmentα∂ofα∂↓↓circumscription↓α∂asα∂aα∂mode
↓ ↓N↓problemα∞andα∞howα∞theyα∞canα∞beα∞representedα∞in         ↓ π∞↓ofα∩reasoningα∩andα∩itsα∩applicationα∪toα∩arti↓↓↓βC↓↓↓cial
↓ ↓N↓theα∞memoryα∂ofα∞aα∂computer,α∞andα∂theα∞heuristic        ↓ π∞↓intelligence.α~ ↓↓Circumscription↓α~formalizesα~the
↓ ↓N↓partα
concernsα
proceduresα
forα
decidingα
whatα
to     ↓ π∞↓processα
ofα
concludingα(oftenα
incorrectly)α
thatαa
↓ ↓N↓doα∂onα∂theα∂basisα∂ofα∂theα∂necessaryα∂facts.α∞ Most       ↓ π∞↓certainα→collectionα→ofα~factsα→isα→allα~thatα→are
↓ ↓N↓workα∞inα∞AIα
hasα∞concernedα∞theα∞↓↓heuristics↓,α
and       ↓ π∞↓relevantα
forαsolvingα
aα
problem.α Itα
doesαthisα
by
↓ ↓N↓computerα∞representationsα
ofα∞informationα
have    ↓ π∞↓allowingα_oneα_toα↔formallyα_assumeα_thatα↔the
↓ ↓N↓α↓ ε↑↓ `2


↓ ↓N↓entititiesα≥thatα≡areα≥generatedα≡byα≥speci↓↓↓βC↓↓↓ed        ↓ π∞↓veri↓↓↓βC↓↓↓cationα⊂willα⊂becomeα∂practicalα⊂inα⊂theα∂very
↓ ↓N↓processesα∃areα∀allα∃theα∀entitiesα∃ofα∃aα∀speci↓↓↓βC↓↓↓ed       ↓ π∞↓nearα⊃future,α⊃butα∩↓↓↓βC↓↓↓rstα⊃weα⊃mustα∩distinguishα⊃it
↓ ↓N↓kind.α⊃ Thisα∩isα⊃commonα⊃inα∩humanα⊃reasoning          ↓ π∞↓from theorem proving by computer.
↓ ↓N↓and,α≠forα≠reasonsα≠describedα≠inα~(McCarthy
↓ ↓N↓1977a),α⊂cannotα∂beα⊂accomplishedα∂byα⊂anyα∂form        ↓ π∞↓Itαisαanα
essentialαpartαofα
theαnotionαofαproofα
in
↓ ↓N↓of deduction.                               ↓ π∞↓aα
formalαsystemα
thatαaα
candidateαproofα
canαbe
                                            ↓ π∞↓checkedα⊗byα⊗aα↔mechanicalα⊗process.α⊗ Itα↔isα⊗a
↓ ↓N↓2.α"Treatingα"conceptsα"asα#objects.α" This,          ↓ π∞↓consequenceα⊃ofα⊃theα⊂workα⊃ofα⊃Goedel,α⊂Church
↓ ↓N↓describedαinα
(McCarthyα1977b),αfacilitates,α
and  ↓ π∞↓andα∩Turingα⊃thatα∩noα⊃mechanicalα∩processα⊃can
↓ ↓N↓mayα#beα#requiredα#for,α#reasoningα"about             ↓ π∞↓alwaysα∞determineα∞whetherα
aα∞proofα∞ofα∞aα
given
↓ ↓N↓knowledge,α!belief,α!wants,α"possibilityα!and       ↓ π∞↓sentenceα≡existsα≡inα≡aα≡formalα∨system.α≡ In
↓ ↓N↓necessity.                                  ↓ π∞↓principle,α∞therefore,α
proof-checkingα∞shouldα
be
                                            ↓ π∞↓easy,αwhileαallαtheαdi↓↓↓β@↓↓↓icultiesαofα
understanding
↓ ↓N↓3.α≠Theα≠currentα~biggestα≠gapα≠inα~computer            ↓ π∞↓theα∞creativeα∞processesα∞ofα∞aα∞mathematicianα
are
↓ ↓N↓reasoningα⊗aboutα↔theα⊗physicalα⊗worldα↔isα⊗the         ↓ π∞↓involvedα∞inα∂makingα∞aα∞highα∂poweredα∞theorem
↓ ↓N↓completeα∂lackα∂ofα∂aα∂systemα∂forα∂reasoningα∞with       ↓ π∞↓prover.
↓ ↓N↓partialα
informationα
aboutα
concurrentα
processes.
↓ ↓N↓Allα↔theα_currentα↔problemα_solvingα↔programs         ↓ π∞↓However,α
inα
spiteα
ofα
theα
simplicityα
ofα
modern
↓ ↓N↓assumeα~thatα~eachα~actionα~ofα~theα→program            ↓ π∞↓logicalα→andα~setα→theoreticα→systemsα~andα→the
↓ ↓N↓producesα∀aα∀nextα∪stateα∀thatα∀dependsα∀onα∪the          ↓ π∞↓brevityα∂withα⊂whichα∂theyα⊂permitα∂axiomatizing
↓ ↓N↓currentα∂state,α∂theα∂action,α∂andα∂sometimesα∂onα∂a      ↓ π∞↓mathematicalα∩andα∩physicalα∪systems,α∩checking
↓ ↓N↓randomα≡variable.α≡ Theyα≡don'tα∨takeα≡into           ↓ π∞↓actualα≤proofsα≤hasα≤encounteredα≠formidable
↓ ↓N↓accountα∂continuousα⊂processesα∂orα∂theα⊂factα∂that     ↓ π∞↓di↓↓↓β@↓↓↓iculties.α∞ Itα∞isα
easyα∞enoughα∞toα∞makeα
proof-
↓ ↓N↓otherα
actionsα
andα
eventsα
mayα
beα
takingα
place.      ↓ π∞↓checkersα⊂forα⊂theα⊂formalα⊂systemsα⊂inα⊂logicα∂and
↓ ↓N↓Weα≥believeα≤thatα≥circumscriptionα≥mayα≤be           ↓ π∞↓setα
theoryα
textbooks,α
andαweα
didα
itα
someαyears
↓ ↓N↓importantα∩inα∪formalizingα∩whatα∪peopleα∩know        ↓ π∞↓ago.α∂ Theα∂di↓↓↓β@↓↓↓icultyα∞isα∂thatα∂theα∂formalα∞proofs
↓ ↓N↓about such processes.                       ↓ π∞↓ofα∀easyα∀theoremsα∀turnα∀outα∀toα∀beα∀tenα∪times
                                            ↓ π∞↓longerαthanαinformalα
proofs,αandαtheα
excessαin
↓ ↓N↓4.α∂Weα∂alsoα∂planα∞someα∂studyα∂ofα∂theα∂theoryα∞of          ↓ π∞↓lengthα
growsα
theα
furtherα
oneα
advancesα
intoα
the
↓ ↓N↓patterns,α∪especiallyα∪higherα∪orderα∀patternsα∪in    ↓ π∞↓theory.α∪ Theα∪troubleα∪isα∪thatα∪mathematicians
↓ ↓N↓whichαfunctionαvariablesαmayαbeαmatchedαand       ↓ π∞↓haveα∞notα∂succeededα∞inα∂completelyα∞formalizing
↓ ↓N↓relationsα∂betweenα∂patternsα∞-α∂forα∂example,α∞the     ↓ π∞↓theα∀languagesα∀andα∀reasoningα∀processesα∀they
↓ ↓N↓relationαbetweenα
aαpatternα
describingαaαtypeα
of    ↓ π∞↓actuallyα⊗use.α⊗ Muchα⊗reasoningα⊗thatα⊗atα∃↓↓↓βC↓↓↓rst
↓ ↓N↓three-dimensionalα
objectα
suchα
asα
aα
personαorα
a     ↓ π∞↓seemsα_toα_beα↔withinα_aα_givenα↔mathematical
↓ ↓N↓vehicleα∪andα∪itsα∪patternsα∪ofα∪itsα∀perceptionα∪-       ↓ π∞↓system,α
actuallyαisα
metamathematicalαreasoning
↓ ↓N↓suchα
asα∞itsα
projectionα
onα∞aα
retinaα∞asα
modi↓↓↓βC↓↓↓ed       ↓ π∞↓aboutα1theα1system.α1 Evenα2whenα1a
↓ ↓N↓byα∂angleα∂ofα∞vision,α∂lightingα∂andα∂occlusionα∞by      ↓ π∞↓mathematicianα
isα
workingα
withinα
aα
system,α
he
↓ ↓N↓other objects.                              ↓ π∞↓establishesα
shortcutsα
whoseα
repeatedα
useα
keeps
                                            ↓ π∞↓down the length of a proof.
↓ ↓N↓Inα allα thisα∨work,α theα emphasisα isα∨on
↓ ↓N↓representationα≠ofα≠theα≠informationα≤thatα≠is        ↓ π∞↓Whenα
weαturnα
toαnon-mathematicalα
reasoning,
↓ ↓N↓actuallyα⊃availableα⊃toα⊂aα⊃personα⊃orα⊃robotα⊂with       ↓ π∞↓presentα#logicalα$systemsα#areα$evenα#more
↓ ↓N↓givenα∩opportunitiesα∩toα∩observeα∩andα⊃compute       ↓ π∞↓inadequateα∞forα∞expressingα∞theα∂reasoningα∞used
↓ ↓N↓and act.                                    ↓ π∞↓inα∨solvingα∨problems.α∨ Weα haveα∨already
                                            ↓ π∞↓identi↓↓↓βC↓↓↓edα≠twoα≠suchα≤inadequacies:α≠problem
↓ ↓N↓α↓ α6Proof-Checking by Computer                  ↓ π∞↓solvingα∩requiresα∩thatα∪conventionalα∩deductive
                                            ↓ π∞↓reasoningα∩interactα∩withα∩observationα∪andα∩use
↓ ↓N↓Computerα
proof-checkingα
isα
neededα
forα
theα
AI      ↓ π∞↓computableα_models,α_andα_circumscriptionα↔as
↓ ↓N↓research,α~andα~itsα~applicationsα~toα~program        ↓ π∞↓describedα∃aboveα∃andα∃inα∃(McCarthyα∃1977a),
↓ ↓N↓α↓ ε↑↓ `3


↓ ↓N↓requiresα
newα∞tools.α
 Theα∞proof-checkerα
allows    ↓ π∞↓(d)α
Weα
checkedα
theα
↓↓↓βC↓↓↓rstα
oneα
hundredα
theorems
↓ ↓N↓usα toα verifyα whetherα ourα axiomsα and               ↓ π∞↓ofα∩setα∪theoryα∩asα∪presentedα∩inα∪(Kelleyα∩1955).
↓ ↓N↓conventionalα⊂rulesα⊂ofα⊂inferenceα⊂togetherα∂with    ↓ π∞↓Thisαestablishedαaα
largeαcollectionαofα
proofsαto
↓ ↓N↓ourαproposedα
newαmethodsα
areαreallyα
adequate      ↓ π∞↓beα
usedα
asα
benchmarksα
toα
measureα
laterα
ideas
↓ ↓N↓toα⊂expressα⊂theα⊂reasoningα⊂requiredα⊂toα⊃solveα⊂a       ↓ π∞↓for shortening proofs.e connecting threads
↓ ↓N↓problem.
                                            ↓ π∞↓(e)α⊂Theα⊂problemα⊂ofα⊂formalizingα⊂howα⊂weα∂can
↓ ↓N↓Weαhaveαaα
proof-checkerαcalledαFOLα(forα
↓↓↓βC↓↓↓rst       ↓ π∞↓reasonα∃aboutα∀whatα∃otherα∀peopleα∃knowα∀was
↓ ↓N↓orderαlogic)α(Weyhrauchα1977a),αweαhaveα
been      ↓ π∞↓studiedα∨byα∨axiomatizingα∨theα "wiseα∨man
↓ ↓N↓improvingα⊃itα⊃sinceα⊃1973,α⊃andα⊃weα∩proposeα⊃to         ↓ π∞↓problem"α⊂(McCarthyα⊂↓↓et.α⊂al↓α⊂1977e)α⊂andα⊂(Sato
↓ ↓N↓improveα'itα'furtherα'underα'thisα&grant.             ↓ π∞↓1977).α∩ Thisα∩wasα∩perhapsα∩theα∪↓↓↓βC↓↓↓rstα∩extended
↓ ↓N↓(Rewritingα
itα
fromα∞scratchα
willα
beα∞requiredα
at     ↓ π∞↓applicationα⊃ofα⊃aα⊃formalizationα⊃ofα⊃knowledge.
↓ ↓N↓someα∞point,α
butα∞weα
aren'tα∞sureα
whenα∞thisα
will       ↓ π∞↓Itα
tookα∞theα
factα
thatα∞theα
↓↓↓βC↓↓↓rstα
andα∞secondα
wise
↓ ↓N↓beα∂theα∂bestα∂useα∂ofα∂limitedα⊂manpower).α∂ With        ↓ π∞↓menα
didn'tα
knowα
theαcolorsα
ofα
theirα
ownαspots
↓ ↓N↓FOL,α#weα#haveα#checkedα#aα#varietyα#of                 ↓ π∞↓asα
hypotheses.α
 Theα
problemα
ofα
provingα
non-
↓ ↓N↓mathematicalα∪proofs,α∪andα∪eachα∀suchα∪project       ↓ π∞↓knowledgeα∀byα∀assumingα∪thatα∀aα∀personα∪only
↓ ↓N↓hasα∞toldα∞usα∞somethingα∞aboutα∞howα∞toα∞improve         ↓ π∞↓knowsα
whatα
followsα
fromα
whatα
heα
isα
statedα
to
↓ ↓N↓theαproof-checkerαorαhowαtoαformalizeαaαgiven      ↓ π∞↓knowα(hasα(notα(beenα(treatedα(inα(the
↓ ↓N↓mathematicalα∀domainα∃orα∀howα∀toα∃writeα∀and           ↓ π∞↓philosophicalα∀orα∪AIα∀literature.α∀ Chrisα∪Goad
↓ ↓N↓debugα∀proofs.α∃ Theα∀proofsα∃describedα∀below        ↓ π∞↓andα'Johnα'McCarthyα'(separately)α&have
↓ ↓N↓eachα∪testedα∪theα∀adequacyα∪ofα∪FOLα∀andα∪our            ↓ π∞↓attackedα
thisα
problem,α
whichα
hasα
turnedαoutα
to
↓ ↓N↓axiomatizations.                            ↓ π∞↓be quite di↓↓↓β@↓↓↓icult and deep.

↓ ↓N↓(a)α⊃Anyα∩deviceα⊃capableα⊃ofα∩acceptingα⊃general       ↓ π∞↓(f)α"Weα!provedα"theα!correctnessα"ofα!the
↓ ↓N↓mathematicalα
reasoningα
mustα
beα
ableα
toαprove      ↓ π∞↓McCarthy-Painterα↔compilerα↔(McCarthyα↔and
↓ ↓N↓theoremsα↔ofα↔arithmetic.α⊗ ↓↓"Ifα↔pα↔isα↔aα⊗prime          ↓ π∞↓Painterα
1967).α
 Thisα
allowedα
usα
toα
compareα
the
↓ ↓N↓↓numberα∞andα∞pα∞dividesα∞theα∞productα∞ab,α∞thenα
p         ↓ π∞↓originalα↔↓↓↓βC↓↓↓rstα↔orderα↔proofα↔withα↔someα↔more
↓ ↓N↓↓dividesα∂aα⊂orα∂pα∂dividesα⊂b."↓α∂isα∂aα⊂typicalα∂simple       ↓ π∞↓recentα∩proofsα∩(Weyhrauchα∩andα∩Milnerα⊃1972;
↓ ↓N↓exampleα∞thatα∂isα∞notα∞justα∂anα∞inductionα∂onα∞the        ↓ π∞↓Boyer and Moore 1975).
↓ ↓N↓statement of the problem.
                                            ↓ π∞↓Afterαaα
periodαofαaddingα
newαfeaturesαtoα
FOL
↓ ↓N↓(b)α∪Theα∪adequacyα∩ofα∪FOL'sα∪setα∪theoryα∩was           ↓ π∞↓weα↔haveα↔againα⊗begunα↔toα↔experimentα⊗with
↓ ↓N↓testedα≥byα≡checkingα≥proofsα≡ofα≥Lagrange's          ↓ π∞↓proofsα)andα*ourα)initialα*successesα)are
↓ ↓N↓theoremα∀andα∀Ramsey'sα∀theorem.α∃ Theseα∀are         ↓ π∞↓encouraging.α! Theseα"recentα!improvements
↓ ↓N↓wellα*knownα)theoremsα*ofα)mathematics.             ↓ π∞↓haveα∞reducedα
theα∞lengthα
ofα∞someα
proofsα∞byα
a
↓ ↓N↓[Lagrange'sα
theorem:α
theα
orderα
ofα
aα
subgroup      ↓ π∞↓factorα
ofα
betterα
thanα
ten.α
 Someα
ofα∞theα
proofs
↓ ↓N↓ofα
aαgroupα
Gα
dividesαtheα
orderα
ofαG;α
Ramsey's        ↓ π∞↓weα⊂areα⊂nowα⊃producingα⊂areα⊂aboutα⊂asα⊃longα⊂as
↓ ↓N↓theorem:α⊂letα⊂Gα⊂beα⊂aα⊂countablyα⊂in↓↓↓βC↓↓↓niteα⊂setα∂of        ↓ π∞↓theirα⊂informalα∂versions.α⊂ Thisα∂isα⊂mostα∂clearly
↓ ↓N↓points,α∩eachα∪pointα∩beingα∩connectedα∪toα∩every       ↓ π∞↓evidentα_inα_theα_↓↓samefringe↓α→exampleα_below.
↓ ↓N↓otherα∂byα⊂aα∂thread,α∂eachα⊂threadα∂beingα⊂redα∂or         ↓ π∞↓Here are three of our recent experiments:
↓ ↓N↓black.α∀ Thenα∃thereα∀isα∃anα∀in↓↓↓βC↓↓↓niteα∃subsetα∀of
↓ ↓N↓theseα∞pointsα∂suchα∞thatα∞theα∂connectingα∞threads     ↓ π∞↓Filmanα(Filman,α
inαprogress)α
hasαusedα
FOLαto
↓ ↓N↓within the subset are all of the same color.]↓ π∞↓showα→thatα→theα→reasoningα→involvedα→inα_the
                                            ↓ π∞↓solutionα
ofα
aα
hardα
retrospectiveα
chessαproblem
↓ ↓N↓(c)α
Wilson'sα
theoremα∞thatα
"Ifα
↓↓p↓α
isα∞prime,α
then      ↓ π∞↓canα∪beα∀formalizedα∪inα∀↓↓↓βC↓↓↓rstα∪orderα∀logic.α∪ We
↓ ↓N↓↓↓p↓α≤dividesα≠↓↓(p-1)!↓"α≤isα≠aα≤purelyα≠arithmetic          ↓ π∞↓choseα
thisα∞exampleα
fromα∞outsideα
mathematics,
↓ ↓N↓statement,α≡butα≡itsα≡proofα≡usesα≡aα≥pairing           ↓ π∞↓becauseα'humanα'reasoningα'oftenα'mixes
↓ ↓N↓argumentα≠(requiringα≠setα≠theory)α≠whichα≠is         ↓ π∞↓deductionα_withα↔observationα_ofα_theα↔outside
↓ ↓N↓beyondα↔theα↔capabilityα↔ofα↔presentα⊗theorem-        ↓ π∞↓world,α↔andα↔observationα⊗ofα↔aα↔chessα⊗↓↓partial
↓ ↓N↓proving programs.
↓ ↓N↓α↓ ε↑↓ ]4


↓ ↓N↓↓position↓α∩isα∩prominentα⊃inα∩thisα∩example.α⊃ The       ↓ π∞↓below).α∀ Thisα∀willα∀beα∀followedα∀byα∃aα∀major
↓ ↓N↓semanticα∂attachmentα⊂mechanismα∂ofα⊂FOLα∂was         ↓ π∞↓e↓↓↓β@↓↓↓ortα⊗toα⊗useα⊗McCarthy'sα↔axiomatizationα⊗of
↓ ↓N↓usedα
toα
buildα
aα
simulationα
ofα
hisα
chessα
world.      ↓ π∞↓LISPα
andα
toα
proveα
propertiesα
ofα
simpleα
LISP
↓ ↓N↓Heα∞couldα∞thenα∞useα∞theα∞semanticα
simpli↓↓↓βC↓↓↓cation      ↓ π∞↓programs.α∃ Weyhrauchα∀hasα∃recentlyα∀pointed
↓ ↓N↓routinesα∂ofα∂FOLα∂toα∂answerα∂(inα∂aα∂singleα∂step)        ↓ π∞↓outα⊂thatα∂thisα⊂sameα⊂techniqueα∂canα⊂beα⊂usedα∂to
↓ ↓N↓questionsα∂likeα∂"isα∂theα∞blackα∂kingα∂inα∂checkα∞on       ↓ π∞↓formulateα∪partα∀ofα∪Danaα∀Scott'sα∪computation
↓ ↓N↓boardα
B"α
byα
lookingαatα
theα
modelα
ratherαthan        ↓ π∞↓inductionα↔intoα⊗↓↓↓βC↓↓↓rstα↔orderα⊗logic.α↔ Thisα⊗also
↓ ↓N↓deducingα
fromα
axiomsα
givingα
theα
positionsα
of      ↓ π∞↓requiresα∨theα∨metamathematicalα≡machinery.
↓ ↓N↓theα
piecesα
andα
othersα
aboutα
theα
rulesα
ofα
chess      ↓ π∞↓Weα∞expectα∞thisα∞toα∞beα∞su↓↓↓β@↓↓↓icientlyα∞practicalα∞for
↓ ↓N↓thatα⊂blackα⊂wasα⊂inα⊂check.α⊂ Thisα⊂singleα⊂useα⊂of        ↓ π∞↓usα
toα
useα
thisα
axiomatizationα
inα
Stanfordα
LISP
↓ ↓N↓semanticα↔attachmentα⊗savesα↔severalα⊗hundred       ↓ π∞↓courses.
↓ ↓N↓stepsα
overα
traditionalα
formalizations.α
 Filman's
↓ ↓N↓proofα⊂isα⊂stillα⊂muchα⊂longerα⊂thanα⊂theα⊂informal       ↓ π∞↓(2)α∂Anotherα∂aspectα∂ofα∂programα⊂veri↓↓↓βC↓↓↓cationα∂is
↓ ↓N↓proof,α≥showingα≥thatα≥weα≥stillα≥don'tα≥fully          ↓ π∞↓whatα≤areα≠calledα≤intensionalα≤propertiesα≠of
↓ ↓N↓understandα
howα
humansα
combineα
observation       ↓ π∞↓programs.α_ Theseα_includeα_thingsα→likeα_how
↓ ↓N↓with deduction.                             ↓ π∞↓muchα
storageα
aα
programα
uses,α
andα
howα
many
                                            ↓ π∞↓stepsα↔itα↔takes.α↔ Theseα↔questionsα↔cannotα⊗be
↓ ↓N↓Weα∂haveα∂preliminaryα∂estimatesα∂ofα⊂theα∂length       ↓ π∞↓askedα
byα
currentα
formalismsα
forα
mathematical
↓ ↓N↓ofα⊗theα⊗Kelleyα⊗setα⊗theoryα⊗proofsα⊗mentioned         ↓ π∞↓theoryα
ofα
computation.α
 Theyα
requireα
theories
↓ ↓N↓above.α∪ Inα∪anα∩initialα∪experimentα∪usingα∩only       ↓ π∞↓thatα
containα
programsα
asα
objectsα
andα
canα
talk
↓ ↓N↓partα∀ofα∪theα∀currentlyα∪availableα∀features,α∪we      ↓ π∞↓aboutα∞theα∞abstractα
propertiesα∞ofα∞theα
machines
↓ ↓N↓reducedα↔theα↔numberα↔ofα↔stepsα↔necessaryα↔to          ↓ π∞↓thatα
theyα
runα
on.α
 Mostα
previousαformalα
e↓↓↓β@↓↓↓orts
↓ ↓N↓proveα
theα
↓↓↓βC↓↓↓rstα
thirty-threeα
theoremsα
fromα
461     ↓ π∞↓haveα
onlyα
shownα
propertiesα
ofα∞theα
algorithms
↓ ↓N↓toα104.α Consideringα
thatαitαtakesαoneα
stepαjust    ↓ π∞↓computedα~byα~programs,α~notα≠propertiesα~of
↓ ↓N↓toα#expressα#theα"theorem,α#thisα#isα"quite             ↓ π∞↓programsα∞themselves.α∞ Oneα∞exceptionα∞wasα
the
↓ ↓N↓impressive.α∞ Weα∞expectα∞thatα∞addingα∞theα
goal-      ↓ π∞↓workαofαAiello,αAiello,αandα
Weyhrauchα(Aiello
↓ ↓N↓structureα#featuresα#mentionedα$belowα#will         ↓ π∞↓1974)α∃onα∃PASCAL.α∃ Thisα∃wasα∃carriedα∀out
↓ ↓N↓substantially reduce these proof lengths.   ↓ π∞↓usingαanotherαformalα
systemαandαweα
haveαjust
                                            ↓ π∞↓begunα
toα
thinkαaboutα
suchα
problemsαusingα
↓↓↓βC↓↓↓rst
↓ ↓N↓Inα)connectionα)withα)McCarthy'sα(recent            ↓ π∞↓orderα logic.α  Oneα∨approachα isα toα∨take
↓ ↓N↓(McCarthyα≥1977d)α≥formalizationα≥ofα≥LISP          ↓ π∞↓advantageα"ofα"theα"factα#thatα"intensional
↓ ↓N↓programsαusingα
sentencesαandα
schemataαofα
↓↓↓βC↓↓↓rst     ↓ π∞↓propertiesα↔ofα↔oneα↔programα↔areα↔extensional
↓ ↓N↓orderα
logic,α
weα
haveα
checkedα
aα
FOLα
proofα
of         ↓ π∞↓properties of certain related programs.
↓ ↓N↓theα⊗correctnessα↔ofα⊗hisα↔↓↓samefringe↓α⊗program.
↓ ↓N↓(↓↓samefringe[x,y]↓α
isα
trueα
ifα
theα
S-expressionsα
↓↓x↓   ↓ π∞↓(3)α→Theα→veri↓↓↓βC↓↓↓cationα→ofα→theα→correctnessα_of
↓ ↓N↓andα
↓↓y↓αhaveα
theα
sameαatomsα
inα
theαsameα
order).        ↓ π∞↓hardwareαcircuitα
designαusingαFOLα
continuing
↓ ↓N↓Theα∪proofα∩asα∪checkedα∪byα∩FOLα∪wasα∪ofα∩the              ↓ π∞↓theα∂workα∞ofα∂Wagnerα∞(Wagnerα∂1977).α∞ Almost
↓ ↓N↓sameαlengthαasαaα
writtenαoutαinformalαproofα
of      ↓ π∞↓allα⊂presentα⊂hardwareα∂veri↓↓↓βC↓↓↓cationα⊂isα⊂basedα∂on
↓ ↓N↓theα≥sameα≡result.α≥ Weα≥believeα≡thatα≥such            ↓ π∞↓simulatingα∪itα∩inα∪allα∩possibleα∪states.α∩ Wagner
↓ ↓N↓favorable results are generally possible.   ↓ π∞↓demonstratedα~thatα→formalα~proofsα~thatα→the
                                            ↓ π∞↓hardwareα⊃isα⊃correctα⊃areα⊃feasibleα⊃andα⊂require
↓ ↓N↓Our plans for FOL include the following:    ↓ π∞↓lessα_humanα_andα_computerα_workα_thanα↔the
                                            ↓ π∞↓simulationα≤techniques.α≤ Inα≤factα≤proofsα≤of
↓ ↓N↓(1)α
Theαveri↓↓↓βC↓↓↓cationα
ofαtheα
correctnessα
ofαLISP     ↓ π∞↓hardwareα∩correctnessα∩areα∩oftenα∩simplerα∩than
↓ ↓N↓programs.α
 Johnα
McCarthyα
(McCarthyα
1977d)       ↓ π∞↓proofsα⊃ofα⊃programα⊃correctness,α⊃becauseα⊃often
↓ ↓N↓hasα∩recentlyα∪begunα∩usingα∩axiomα∪schemasα∩to         ↓ π∞↓mathematical induction is not required.
↓ ↓N↓proveα∂theα∂propertiesα∂ofα∂LISPα⊂programs.α∂ We
↓ ↓N↓intendα∪toα∪expandα∪thisα∪workα∀byα∪introducing         ↓ π∞↓(4)α
Weα
intendα∞toα
redoα
theα
theoremsα∞ofα
Kelley
↓ ↓N↓meta-mathematicalα⊃machineryα⊃intoα⊃FOLα⊃(see       ↓ π∞↓mentionedαaboveαusingαtheαmanyαnewαfeatures
↓ ↓N↓α↓ ε↑↓ ←5


↓ ↓N↓thatαhaveα
beenαaddedα
toαFOL.α
 Theseαinclude        ↓ π∞↓interest,α⊃andα∩weα⊃proposeα⊃aα∩rotatingα⊃research
↓ ↓N↓theα/syntacticα.simpli↓↓↓βC↓↓↓er,α/theα.semantic           ↓ π∞↓associateshipα⊗forα∃recentα⊗PhDsα⊗interestedα∃in
↓ ↓N↓attachmentα∩mechanism,α⊃andα∩variousα⊃decision      ↓ π∞↓contributing to the work and learning from it.
↓ ↓N↓procedures.
                                            ↓ π∞↓α↓ 	↓Facilities 
↓ ↓N↓(5)α∪Introducingα∀metamathematicalα∪machinery
↓ ↓N↓intoα∪FOLα∩willα∪allowα∪usα∩toα∪stateα∪andα∩prove           ↓ π∞↓Theα⊗projectα↔willα⊗beα↔partα⊗ofα↔theα⊗Stanford
↓ ↓N↓theoremsα⊂aboutα⊂howα∂weα⊂doα⊂reasoningα⊂inα∂the          ↓ π∞↓Universityα_Arti↓↓↓βC↓↓↓cialα_Intelligenceα↔Laboratory
↓ ↓N↓logic.α≠ Inα~particular,α≠weα~willα≠beα≠ableα~to          ↓ π∞↓andα_willα↔useα_itsα↔computerα_facilities.α↔ This
↓ ↓N↓establish,αasα
sentencesαofα
theαmetamathematics,  ↓ π∞↓LaboratoryαisαdirectedαbyαJohnαMcCarthyαand
↓ ↓N↓newα↔axiomα_schemasα↔thatα_canα↔beα_usedα↔in              ↓ π∞↓hasα∂beenα∞mainlyα∂supportedα∞byα∂ARPAα∂inα∞the
↓ ↓N↓furtherα∞proofs.α∞ Thisα∞willα∞beα∂especiallyα∞useful   ↓ π∞↓past,α∞butα∞theα∞fractionα∞ofα∞itsα∞supportα
provided
↓ ↓N↓inα provingα theα correctnessα!ofα recursive          ↓ π∞↓by ARPA is diminishing.
↓ ↓N↓programs.α∞ Anotherα∞applicationα∞ofα∞schemasα∞is
↓ ↓N↓to axiomatizing circumscription.            ↓ π∞↓Theα∞Laboratoryα∞computerα∞facilityα∞isα
generally
                                            ↓ π∞↓adequateαforα
thisαworkαandα
thereαareαnoα
direct
↓ ↓N↓(6)α
Theα
usefulnessα
ofα
theα
metamathematicsα
will    ↓ π∞↓chargesα∪forα∩computerα∪timeα∩inα∪thisα∩proposal.
↓ ↓N↓beα∩enhancedα∪byα∩certainα∪re↓↓↓βD↓↓↓ectionα∩principles.     ↓ π∞↓However,α∂thereα∂areα∂budgetα∂itemsα∂forα∂aα∂share
↓ ↓N↓Theseα≠areα≠rulesα~thatα≠stateα≠someα~relation          ↓ π∞↓ofα∞aα∂computerα∞technicianα∞andα∂someα∞computer
↓ ↓N↓betweenα∃aα∃theoryα∃andα∃itsα∃metamathematics.        ↓ π∞↓maintenanceα∞costs.α
 Inα∞addition,α
thereα∞areα
two
↓ ↓N↓Forα∩example,α∩ifα∪youα∩haveα∩provedα∪aα∩certain          ↓ π∞↓computerαterminalsαbudgetedαatα$2,500α
eachαto
↓ ↓N↓formula,α⊗thenα⊗inα⊗theα⊗meta-theoryα⊗youα∃can          ↓ π∞↓provideα
remoteα
accessα
toα
theα
computerα
forα
the
↓ ↓N↓assertα)thatα)theα)formulaα)isα(provable.             ↓ π∞↓participantsα∞inα
thisα∞project.α
 Theα∞totalα∞costα
of
↓ ↓N↓Conversely,α∩informalα∩mathematicsα∪oftenα∩uses     ↓ π∞↓computerα∃facilitiesα∀providedα∃inα∀thisα∃wayα∀is
↓ ↓N↓metamathematicalα∂assertionsα∞thatα∂allα∞formulas   ↓ π∞↓substantiallyαlessα
thanαitαwouldα
beαonαtheα
basis
↓ ↓N↓withα#certainα#propertiesα#areα#true.α# The           ↓ π∞↓of direct charges for computer time used.
↓ ↓N↓attachmentα0mechanismα0combinedα/with
↓ ↓N↓re↓↓↓βD↓↓↓ectionα)principlesα(willα)allowα)usα(to            ↓ π∞↓α↓ λ}Personnel 
↓ ↓N↓automaticallyα
useα
suchα
metatheoremsα
toα
prove
↓ ↓N↓theorems in the base theory.                ↓ π∞↓α↓ πwBiography of John McCarthy 

↓ ↓N↓α↓ αSOrganization of the work                    ↓ π∞↓BORN: September 4, 1927 in Boston,
                                            ↓ π∞↓↓ πNMassachusetts
↓ ↓N↓Theα⊃workα∩isα⊃underα∩theα⊃generalα∩directionα⊃of
↓ ↓N↓Johnα2McCarthyα1whoα2alsoα1develops                 ↓ π∞↓EDUCATION:
↓ ↓N↓formalizationsα∀andα∀generalα∀theoryα∃andα∀uses       ↓ π∞↓B.S.  (Mathematics) California Institute of
↓ ↓N↓FOLα∃toα∃checkα∃outα∃formalizations.α∀ Richard        ↓ π∞↓↓ πNTechnology, 1948.
↓ ↓N↓Weyhrauchα⊗isα⊗theα⊗mainα⊗developerα↔ofα⊗and            ↓ π∞↓Ph.D. (Mathematics) Princeton University,
↓ ↓N↓implementerα∃ofα∃FOLα∃andα∃isα∃alsoα∃pursuing           ↓ π∞↓↓ πN1951.
↓ ↓N↓researchα⊗makingα↔metamathematicalα⊗methods
↓ ↓N↓availableα∂inα⊂it.α∂ Graduateα∂studentsα⊂helpα∂with     ↓ π∞↓HONORS AND SOCIETIES:
↓ ↓N↓implementationsα
andα
pursueα
thesisα
researchαin    ↓ π∞↓American Mathematical Society,
↓ ↓N↓arti↓↓↓βC↓↓↓cialα1intelligenceα2(concentratingα1on       ↓ π∞↓Association for Computing Machinery,
↓ ↓N↓epistemologicalαproblems)αandαinα
mathematical   ↓ π∞↓Sigma Xi,
↓ ↓N↓theoryα↔ofα↔computation.α↔ Theα_groupα↔shares         ↓ π∞↓Sloan Fellow in Physical Science (1957-59),
↓ ↓N↓interestsα
withα
theα
separatelyα
supportedα
groups   ↓ π∞↓ACM National Lecturer (1961),
↓ ↓N↓inα∪mathematicalα∪theoryα∪ofα∀computationα∪and        ↓ π∞↓IEEE,
↓ ↓N↓theoremα∞proving.α∞ Bothα∞theα∞epistemologyα∞and      ↓ π∞↓A.M. Turing Award from Association for
↓ ↓N↓theαproof-checkingα
haveαexcitedα
muchαoutside     ↓ π∞↓↓ πNComputing Machinery (1971).
↓ ↓N↓α↓ ε↑↓ `6


↓ ↓N↓PROFESSIONAL EXPERIENCE:                    ↓ π∞↓[5] "Problems in the Theory of Computation",
↓ ↓N↓Proctor Fellow, Princeton University (1950- ↓ π∞↓↓ πN↓↓Proc. IFIP Congress 1965↓.
↓ ↓N↓↓ α∞51),                                        ↓ π∞↓[6] "Time-Sharing Computer Systems", in W.
↓ ↓N↓Higgins Research Instructor in Mathematics, ↓ π∞↓↓ πNOrr (ed.), ↓↓Conversational Computers↓,
↓ ↓N↓↓ α∞Princeton University (1951-53),             ↓ π∞↓↓ πNWiley, 1966.
↓ ↓N↓Acting Assistant Professor of Mathematics,  ↓ π∞↓[7] "A Formal Description of a Subset of
↓ ↓N↓↓ α∞Stanford University (1953-55),              ↓ π∞↓↓ πNAlgol", in T.  Steele (ed.), ↓↓Formal
↓ ↓N↓Assistant Professor of Mathematics,         ↓ π∞↓↓↓ πNLanguage Description Languages for
↓ ↓N↓↓ α∞Dartmouth College (1955-58),                ↓ π∞↓↓↓ πNComputer Programming↓, North-Holland,
↓ ↓N↓Assistant Professor of Communication Science,↓ π∞↓↓ πNAmsterdam, 1966.
↓ ↓N↓↓ α∞M.I.T. (1958-61),                           ↓ π∞↓[8] "Information", ↓↓Scienti↓↓βS↓↓↓c American↓,
↓ ↓N↓Associate Professor of Communication        ↓ π∞↓↓ πNSeptember 1966.
↓ ↓N↓↓ α∞Science, M.I.T. (1961-62),                  ↓ π∞↓[9] "Computer Control of a Hand and Eye", in
↓ ↓N↓Professor of Computer Science Stanford      ↓ π∞↓↓ πN↓↓Proc.  Third All-Union Conference on
↓ ↓N↓↓ α∞University (1962 - present).                ↓ π∞↓↓↓ πNAutomatic Control (Technical Cybernetics)↓,
                                            ↓ π∞↓↓ πNNauka, Moscow, 1967 (Russian).
↓ ↓N↓PROFESSIONAL RESPONSIBILITIES               ↓ π∞↓[10] (with D. Brian, G. Feldman, and J. Allen)
↓ ↓N↓↓ α∞AND SCIENTIFIC INTERESTS:                   ↓ π∞↓↓ πN"THOR ↓↓↓βE↓↓↓ A Display Based Time-
↓ ↓N↓With Marvin Minsky organized and directed   ↓ π∞↓↓ πNSharing System", ↓↓Proc. AFIPS Conf.↓
↓ ↓N↓↓ α∞the Arti↓↓↓βC↓↓↓cial Intelligence Project at       ↓ π∞↓↓ πN(FJCC), Vol.  30, Thompson,
↓ ↓N↓↓ α∞M.I.T.                                      ↓ π∞↓↓ πNWashington, D.C., 1967.
↓ ↓N↓Organized and directs Stanford Arti↓↓↓βC↓↓↓cial    ↓ π∞↓[11] (with James Painter) "Correctness of a
↓ ↓N↓↓ α∞Intelligence Project.                       ↓ π∞↓↓ πNCompiler for Arithmetic Expressions",
↓ ↓N↓Developed the LISP programming system for   ↓ π∞↓↓ πNAmer. Math. Soc., ↓↓Proc. Symposia in
↓ ↓N↓↓ α∞computing with symbolic expressions,        ↓ π∞↓↓↓ πNApplied Math., Math. Aspects of
↓ ↓N↓within the subset are all of the same color.]↓ π∞↓↓↓ πNComputer Science↓, New York, 1967.
↓ ↓N↓(c) Wilson's theorem that "If ↓↓p↓ is prime, then↓ π∞↓[12] "Programs with Common Sense", in
↓ ↓N↓↓↓p↓ divides ↓↓(p-1)!↓" is a purely arithmetic    ↓ π∞↓↓ πNMarvin Minsky (ed.), ↓↓Semantic
↓ ↓N↓statement, but its proof uses a pairing     ↓ π∞↓↓↓ πNInformation Processing↓, MIT Press,
↓ ↓N↓argument (requiring set theory) which is    ↓ π∞↓↓ πNCambridge, 1968.
↓ ↓N↓beyond the capability of present theorem-   ↓ π∞↓[13] (with Lester Earnest, D. Raj. Reddy,
↓ ↓N↓proving programs.                           ↓ π∞↓↓ πNPierre Vicens) "A Computer with Hands,
↓ ↓N↓(d) We checked the ↓↓↓βC↓↓↓rst one hundred theorems↓ π∞↓↓ πNEyes, and Ears", ↓↓Proc. AFIPS Conf.↓
↓ ↓N↓of set theory as presented in (Kelley 1955).↓ π∞↓↓ πN(FJCC), 1968.
↓ ↓N↓This established a large collection of proofs to↓ π∞↓[14] (with Patrick Hayes) "Some Philosophical
↓ ↓N↓be used as benchmarks to measure later ideas↓ π∞↓↓ πNProblems from the Standpoint of
↓ ↓N↓for shortening proofs.                      ↓ π∞↓↓ πNArti↓↓↓βC↓↓↓cial Intelligence", in Donald Michie
↓ ↓N↓[2] "A Basis for a Mathematical Theory of   ↓ π∞↓↓ πN(ed.), ↓↓Machine Intelligence 4↓, American
↓ ↓N↓↓ α∞Computation", in P. Bra↓↓↓β@↓↓↓ort and D.          ↓ π∞↓↓ πNElsevier, New York, 1969.
↓ ↓N↓↓ α∞Hershberg (eds.), ↓↓Computer Programming      ↓ π∞↓[15] "The Home Information Terminal", ↓↓Man
↓ ↓N↓↓↓ α∞and Formal Systems↓, North-Holland,          ↓ π∞↓↓↓ πNand Computer, Proc. Int. Conf.,
↓ ↓N↓↓ α∞Amsterdam, 1963.                            ↓ π∞↓↓↓ πNBordeaux, 1970↓, S. Karger, New York,
↓ ↓N↓[3] (with S. Boilen, E. Fredkin, J.C.R.     ↓ π∞↓↓ πN1972.
↓ ↓N↓↓ α∞Licklider) "A Time-Sharing Debugging        ↓ π∞↓[16] "Mechanical Servants for Mankind," in
↓ ↓N↓↓ α∞System for a Small Computer", ↓↓Proc.         ↓ π∞↓↓ πN↓↓Britannica Yearbook of Science and the
↓ ↓N↓↓↓ α∞AFIPS Conf.↓ (SJCC), Vol. 23, 1963.          ↓ π∞↓↓↓ πNFuture↓, 1973.
↓ ↓N↓[4] (with F. Corbato, M. Daggett) "The      ↓ π∞↓[17] Book Review: "Arti↓↓↓βC↓↓↓cial Intelligence: A
↓ ↓N↓↓ α∞Linking Segment Subprogram Language         ↓ π∞↓↓ πNGeneral Survey" by Sir James Lighthill,
↓ ↓N↓↓ α∞and Linking Loader Programming              ↓ π∞↓↓ πNin ↓↓Arti↓↓βS↓↓↓cial Intelligence, Vol. 5, No. 3↓,
↓ ↓N↓↓ α∞Languages", ↓↓Comm. ACM↓, July 1963.           ↓ π∞↓↓ πNFall 1974.
↓ ↓N↓α↓ ε↑↓ `7


↓ ↓N↓[18] "Modeling Our Minds" in ↓↓Science Year   ↓ π∞↓↓↓ πNArti↓↓βS↓↓↓cial Intelligence↓, M.I.T., Cambridge,
↓ ↓N↓↓↓ α∞1975↓, The World Book Science Annual,        ↓ π∞↓↓ πN1977.
↓ ↓N↓↓ α∞Field Enterprises Educational
↓ ↓N↓↓ α∞Corporation, Chicago, 1974.                 ↓ π∞↓α↓ πABiography of Richard W. Weyhrauch 
↓ ↓N↓[19] "The Home Information Terminal,"
↓ ↓N↓↓ α∞invited presentation, AAAS Annual           ↓ π∞↓BORN: 3 July 1943, Blue Point, New York
↓ ↓N↓↓ α∞Meeting, Feb. 18-24, 1976, Boston.
↓ ↓N↓[20] "An Unreasonable Book," a review of    ↓ π∞↓EDUCATION
↓ ↓N↓↓ α∞↓↓Computer Power and Human Reason↓, by
↓ ↓N↓↓ α∞Joseph Weizenbaum (W.H. Freeman and         ↓ π∞↓1975 Ph.D. Stanford University Mathematics
↓ ↓N↓↓ α∞Co., San Francisco, 1976) in SIGART         ↓ π∞↓1965 B.S. New York University Mathematics
↓ ↓N↓↓ α∞Newsletter
↓ ↓N↓558, June 1976, also in ↓↓Creative Computing↓, ↓ π∞↓PROFESSIONAL EXPERIENCE
↓ ↓N↓↓ α∞Chestnut Hill, Massachusetts, 1976 and in
↓ ↓N↓↓ α∞"Three Reviews of J. Weizenbaum's           ↓ π∞↓1971-present Research Associate, Arti↓↓↓βC↓↓↓cial
↓ ↓N↓↓ α∞↓↓Computer Power and Human Reason↓,            ↓ π∞↓↓ πNIntelligence Lab, Stanford University
↓ ↓N↓↓ α∞(with B. Buchanan and J. Lederberg),        ↓ π∞↓↓ πNConsultant for IBM, Tymshare, Intel,
↓ ↓N↓↓ α∞Stanford Arti↓↓↓βC↓↓↓cial Intelligence             ↓ π∞↓↓ πNvarious governmental agencies.
↓ ↓N↓↓ α∞Laboratory Memo 291, Computer Science
↓ ↓N↓↓ α∞Department, Stanford, November 1976.        ↓ π∞↓RESEARCH INTERESTS
↓ ↓N↓[21] Review: ↓↓Computer Power and Human       ↓ π∞↓Arti↓↓↓βC↓↓↓cial intelligence, in particular,
↓ ↓N↓↓↓ α∞Reason↓, by Joseph Weizenbaum (W.H.          ↓ π∞↓↓ πNmathematical logic as a tool in the
↓ ↓N↓↓ α∞Freeman and Co., San Francisco, 1976) in    ↓ π∞↓↓ πNdevelopment of programs to simulate
↓ ↓N↓↓ α∞Physics Today, 1977.                        ↓ π∞↓↓ πNhuman reasoning.
↓ ↓N↓[22] "The Home Information Terminal" to
↓ ↓N↓↓ α∞appear in The Grolier Encyclopedia,         ↓ π∞↓PUBLICATIONS:
↓ ↓N↓↓ α∞1977, also to appear in ↓↓The International   ↓ π∞↓[1] Weyhrauch, Richard, and Milner, Robin,
↓ ↓N↓↓↓ α∞YearBook and Statemen's Who's Who↓,          ↓ π∞↓↓ πN"Program Semantics andCorrectness in a
↓ ↓N↓↓ α∞Surrey, England, 1977.                      ↓ π∞↓↓ πNMechanized Logic", ↓↓Proc. USA-Japan
↓ ↓N↓[23] "Dialnet and Home Computers" (with Les ↓ π∞↓↓↓ πNComputer Conference↓, Tokyo, 1972.
↓ ↓N↓↓ α∞Earnest), ↓↓Proceedings of the First West     ↓ π∞↓[2] Milner, Robin, and Weyhrauch, Richard,
↓ ↓N↓↓↓ α∞Coast Computer Faire and Conference↓,        ↓ π∞↓↓ πN"Proving Compiler Correctness in a
↓ ↓N↓↓ α∞San Francisco, April 1977.                  ↓ π∞↓↓ πNMechanized Logic", ↓↓Machine Intelligence
↓ ↓N↓[24] "On The Model Theory of Knowledge"     ↓ π∞↓↓↓ πN7↓, Edinburgh University Press, 1972.
↓ ↓N↓↓ α∞(with M. Sato, S. Igarashi, and T.          ↓ π∞↓[3] Anderson, D.B., Binford, T.O., Thomas,
↓ ↓N↓↓ α∞Hayashi), ↓↓Proceedings of the Fifth          ↓ π∞↓↓ πNA.J., Weyhrauch, R.W., and Wilks, Y.A.,
↓ ↓N↓↓↓ α∞International Joint Conference on           ↓ π∞↓↓ πN"AFTER LEIBNIZ . . . : Discussions on
↓ ↓N↓↓↓ α∞Arti↓↓βS↓↓↓cial Intelligence↓, M.I.T, Cambridge,   ↓ π∞↓↓ πNPhilosophy and Arti↓↓↓βC↓↓↓cial Intelligence"
↓ ↓N↓↓ α∞1977.                                       ↓ π∞↓↓ πNStanford Arti↓↓↓βC↓↓↓cial Intelligence
↓ ↓N↓[25] "Another SAMEFRINGE", in SIGART        ↓ π∞↓↓ πNLaboratory Memo AIM-229, Stanford
↓ ↓N↓↓ α∞Newsletter No. 61, February 1977.           ↓ π∞↓↓ πNUniversity, April 1974.
↓ ↓N↓[26] "Ascribing Mental Qualities to Machines"↓ π∞↓[4] Aiello, Luiga, and Weyhrauch, Richard,
↓ ↓N↓↓ α∞to appear in ↓↓Essays in Philosophy and       ↓ π∞↓↓ πN"LCFsmall: an Implementation of LCF"
↓ ↓N↓↓↓ α∞Computer Technology↓, National               ↓ π∞↓↓ πNStanford Arti↓↓↓βC↓↓↓cial Intelligence
↓ ↓N↓↓ α∞Symposium for Philosophy and                ↓ π∞↓↓ πNLaboratory Memo AIM-241, Stanford
↓ ↓N↓↓ α∞Computer Technology, New York, 1977.        ↓ π∞↓↓ πNUniversity, August 1974.
↓ ↓N↓[27] "Epistemological Problems of Arti↓↓↓βC↓↓↓cial ↓ π∞↓[5] Aiello, Mario, and Weyhrauch, Richard,
↓ ↓N↓↓ α∞Intelligence", ↓↓Proceedings of the Fifth     ↓ π∞↓↓ πN"Checking Proofs in the
↓ ↓N↓↓↓ α∞International Joint Conference on           ↓ π∞↓↓ πNMetamathematics of First Order Logic"
↓ ↓N↓α↓ ε↑↓ ←8


↓ ↓N↓↓ α∞Stanford Arti↓↓↓βC↓↓↓cial Intelligence
↓ ↓N↓↓ α∞Laboratory Memo AIM-222, Stanford
↓ ↓N↓↓ α∞University, August 1974.
↓ ↓N↓[6] Weyhrauch, Richard, and Thomas,
↓ ↓N↓↓ α∞Arthur, "FOL: A Proof Checker for
↓ ↓N↓↓ α∞First-order Logic" Stanford Arti↓↓↓βC↓↓↓cial
↓ ↓N↓↓ α∞Intelligence Laboratory Memo AIM-235,
↓ ↓N↓↓ α∞Stanford University, September 1974.
↓ ↓N↓[7] Aiello, Luiga, Aiello, Mario, and
↓ ↓N↓↓ α∞Weyhrauch, Richard, "The Semantics of
↓ ↓N↓↓ α∞PASCAL in LCF" Stanford Arti↓↓↓βC↓↓↓cial
↓ ↓N↓↓ α∞Intelligence Laboratory Memo AIM-221,
↓ ↓N↓↓ α∞Stanford University, October 1974.
↓ ↓N↓[8] Weyhrauch, Richard, W.  "Relations
↓ ↓N↓↓ α∞Between Some Hierarchies of Ordinal
↓ ↓N↓↓ α∞Functions and Functionals", Ph.D.
↓ ↓N↓↓ α∞Dissertation, Stanford University,
↓ ↓N↓↓ α∞Stanford, California, November 1975.
↓ ↓N↓[9] Filman, Robert and Weyhrauch, Richard,
↓ ↓N↓↓ α∞"An FOL Primer" Stanford Arti↓↓↓βC↓↓↓cial
↓ ↓N↓↓ α∞Intelligence Laboratory Memo AIM-288,
↓ ↓N↓↓ α∞Stanford University, September 1976.
↓ ↓N↓[10] Weyhrauch, Richard W., "FOL: A Proof
↓ ↓N↓↓ α∞Checker for First-order Logic" Stanford
↓ ↓N↓↓ α∞Arti↓↓↓βC↓↓↓cial Intelligence Laboratory Memo
↓ ↓N↓↓ α∞AIM-235.1, Stanford University, August
↓ ↓N↓↓ α∞1977.
↓ ↓N↓α↓ ε↑↓ `9


↓ ↓N↓α↓ ε/Budget 

↓ ↓N↓∧PERIOD COVERED: 3 Years: 1 Jan. 1978 through 31 December 1980.

↓ ↓N↓∧Dates:                     1/1/78-12/31/78   1/1/79-12/31/79   1/1/80-12/31/80

↓ ↓N↓∧                                   Person-           Person-          Person-
↓ ↓N↓∧A. SALARIES AND WAGES              months            months           months

↓ ↓N↓∧   1. Senior Personnel:

↓ ↓N↓∧     a. John McCarthy,     7,575.    9.0     8,181.    9.0    8,835.    9.0
↓ ↓N↓∧       Professor
↓ ↓N↓∧       Summer 75%
↓ ↓N↓∧       Acad. Yr. 0%

↓ ↓N↓∧   2. Other Personnel

↓ ↓N↓∧     a. Research Associates

↓ ↓N↓∧       (1) R. Weyhrauch   10,400.    6.0    11,232.    6.0   12,131.    6.0
↓ ↓N↓∧          50% - 12 months
↓ ↓N↓∧                                
↓ ↓N↓∧       (2) ________,      17,000.   12.0    18,360.   12.0   19,829.   12.0
↓ ↓N↓∧          100% - 12 months

↓ ↓N↓∧     b. Student Research 
↓ ↓N↓∧        Assistants
↓ ↓N↓∧        (50% Acad.Yr.;               4.5               4.5              4.5
↓ ↓N↓∧        100% Summer)                 3.0               3.0              3.0

↓ ↓N↓∧       (1)                 7,155.            7,704.           8,320.       

↓ ↓N↓∧       (2)                 7,155.            7,704.           8,320.       

↓ ↓N↓∧     c. Support Personnel

↓ ↓N↓∧       (1) Sec'y (25%)     2,615.    3.0     2,824.    3.0    3,050.    3.0

↓ ↓N↓∧       (2) Elec.Tech.(25%) 4,895.    3.0     5,287.    3.0    5,710.    3.0
↓ ↓N↓∧                          _______           _______          _______

↓ ↓N↓∧   Total Salaries & Wages 56,795.           61,292.          66,195.

↓ ↓N↓∧B. STAFF BENEFITS         
↓ ↓N↓∧   9/1/77-8/31/78:20.0%          
↓ ↓N↓∧   9/1/78-8/31/79:20.8%
↓ ↓N↓∧   9/1/79-8/31/80;21.6%                                          
↓ ↓N↓∧   9/1/80-8/31/81;22.4%
↓ ↓N↓∧                          11,510.           12,912.          14,475.
↓ ↓N↓∧                          _______          ________         ________
↓ ↓N↓∧C. TOTAL SALARIES, WAGES,
↓ ↓N↓∧   AND STAFF BENEFITS     68,305.           74,204.          80,670.
↓ ↓N↓α↓ ε↑↓ P10


↓ ↓N↓∧D. PERMANENT EQUIPMENT     5,000                --               --
↓ ↓N↓∧   (2 Datamedia terminals)

↓ ↓N↓∧E. EXPENDABLE SUPPLIES     2,040.            2,040.           2,040.
↓ ↓N↓∧   & EQUIPMENT(e.g.,copying,
↓ ↓N↓∧   office supplies, postage,      
↓ ↓N↓↓ α∞participated in the development of the
↓ ↓N↓↓ α∞ALGOL 58 and the ALGOL 60
↓ ↓N↓↓ α∞languages.
↓ ↓N↓Present scienti↓↓↓βC↓↓↓c work is in the ↓↓↓βC↓↓↓elds of
↓ ↓N↓↓ α∞Arti↓↓↓βC↓↓↓cial Intelligence, Computation with
↓ ↓N↓↓ α∞Symbolic Expressions, Mathematical
↓ ↓N↓↓ α∞Theory of Computation, Time-Sharing
↓ ↓N↓↓ α∞computer systems.
↓ ↓N↓PUBLICATIONS:
↓ ↓N↓[1] "Towards a Mathematical Theory of
↓ ↓N↓↓ α∞Computation", in ↓↓Proc. IFIP Congress
↓ ↓N↓↓↓ α∞62↓, North-Holland, Amsterdam, 1963.
↓ ↓N↓∧      Equip. Maint.
↓ ↓N↓∧                          _______          ________          _______  

↓ ↓N↓∧I. TOTAL COSTS             87,145.          88,044.          94,510.
↓ ↓N↓∧    (A through H)

↓ ↓N↓∧J. INDIRECT COSTS:58% of   47,644.          51,066.          54,816.
↓ ↓N↓∧   A through H, less D.   ________         ________         ________     


↓ ↓N↓∧K. TOTAL COSTS            134,789.         139,110.         149,326.

↓ ↓N↓∧L. THREE YEAR TOTAL                                         423,225.
↓ ↓N↓α↓ ε↑↓ V11


↓ ↓N↓α↓ β5References                                  ↓ π∞↓↓ π>Available as <Arpanet:SAIL>
                                            ↓ π∞↓↓ π>MENTAL.[F76,JMC].
↓ ↓N↓↓αAiello, L., Aiello, M., and Weyhrauch, R.↓
↓ ↓N↓↓ ↓}(1974) The Semantics of PASCAL in           ↓ π∞↓↓αMcCarthy, J. ↓ (1977d) First-Order
↓ ↓N↓↓ ↓}LCF, Stanford: Stanford AI Memo             ↓ π∞↓↓ π>Representation of Recursive Programs, (to
↓ ↓N↓↓ ↓}AIM-221.  Available as <Arpanet:SAIL>       ↓ π∞↓↓ π>be published).  Available as
↓ ↓N↓↓ ↓}AIM221.PUB[DOC,RWW].                        ↓ π∞↓↓ π><Arpanet:SAIL> FIRST.NEW[W77,JMC].

↓ ↓N↓↓αBoyer, R.S., and Moore, J.S.↓ (1975) Proving ↓ π∞↓↓αMcCarthy, J., Sato, M., Hayashi, T. and
↓ ↓N↓↓ ↓}Theorems About LISP Functions, JACM         ↓ π∞↓α↓ π>Igarashi, S.↓ (1977e) On the Model Theory
↓ ↓N↓↓ ↓}Vol 22. No. 1 pp. 129-144. New York:        ↓ π∞↓↓ π>of Knowledge.  Presented at ↓↓IJCAI-1977↓;
↓ ↓N↓↓ ↓}ACM.                                        ↓ π∞↓↓ π>to appear in the ↓↓SIGART Newsletter↓.

↓ ↓N↓↓αFilman, R.E.↓ (in progress) Explorations in  ↓ π∞↓↓αMoore, Robert C.↓ (1977) Reasoning about
↓ ↓N↓↓ ↓}Representations: The Chess Domain.          ↓ π∞↓↓ π>Knowledge and Action, ↓↓1977 IJCAI
                                            ↓ π∞↓↓↓ π>Proceedings↓.  Available as
↓ ↓N↓↓αGoad, Christopher↓ (in progress) A Model     ↓ π∞↓↓ π><Arpanet:SAIL> IJCAI.PUB[1,RCM].
↓ ↓N↓↓ ↓}Theoretic Solution of the Wise Man
↓ ↓N↓↓ ↓}Problem.                                    ↓ π∞↓↓αSato, M.↓ (1977) A study of Kripke-type
                                            ↓ π∞↓↓ π>Models for some Model Logics by
↓ ↓N↓↓αKelley, J.L.↓ (1955) General Topology,       ↓ π∞↓↓ π>Gentzen's Sequential Method, (to appear
↓ ↓N↓↓ ↓}Princeton, New Jersey: D. Van Nostrand      ↓ π∞↓↓ π>in Publ. R.I.M.S., Kyoto University).
↓ ↓N↓↓ ↓}Company, Inc.
                                            ↓ π∞↓↓αWagner, Todd J.↓ (1977) Hardware
↓ ↓N↓↓αMcCarthy, J. and Painter, J.↓ (1967)         ↓ π∞↓↓ π>Veri↓α↓βC↓α↓cation.  Ph.D. thesis, Stanford
↓ ↓N↓↓ ↓}Correctness of a Compiler for Arithmetic    ↓ π∞↓↓ π>University.  Available as <Arpanet:SAIL>
↓ ↓N↓↓ ↓}Expressions.  ↓↓Proc. Symposia in Applied     ↓ π∞↓↓ π>THESIS.PUB[THE,TJW].
↓ ↓N↓↓↓ ↓}Math., Math. Aspects of Computer
↓ ↓N↓↓↓ ↓}Science↓ New York: Amer. Math. Soc..         ↓ π∞↓↓αWeyhrauch, R. W., and Milner, R.↓ (1972)
                                            ↓ π∞↓↓ π>Program Semanantics and Correctness in a
↓ ↓N↓↓αMcCarthy, J. and Hayes, P.J.↓ (1969) Some    ↓ π∞↓↓ π>Mechanized Logic.  ↓↓First USA - Japan
↓ ↓N↓↓ ↓}Philosophical Problems from the             ↓ π∞↓↓↓ π>Computer Conference Proceedings.↓ Tokyo:
↓ ↓N↓↓ ↓}Standpoint of Arti↓α↓βC↓α↓cial Intelligence.       ↓ π∞↓↓ π>Hitachi Priniting Company.
↓ ↓N↓↓ ↓}↓↓Machine Intelligence 4↓, pp. 463-502 (eds
↓ ↓N↓↓ ↓}Meltzer, B. and Michie, D.). Edinburgh:     ↓ π∞↓↓αWeyhrauch, R. W.↓ (1977a) A Users Manual
↓ ↓N↓↓ ↓}Edinburgh University Press.                 ↓ π∞↓↓ π>for FOL. Stanford: Stanford AI Memo
                                            ↓ π∞↓↓ π>AIM-235.1.  Available as <Arpanet:SAIL>
↓ ↓N↓↓αMcCarthy, J.↓ (1977a) Minimal Inference - A  ↓ π∞↓↓ π>FOLMAN.PUB[DOC,RWW].
↓ ↓N↓↓ ↓}New Way of Jumping to Conclusions (to
↓ ↓N↓↓ ↓}be published).  Available as                ↓ π∞↓↓αWeyhrauch, R. W. (ed.)↓ (1977b) A Collection
↓ ↓N↓↓ ↓}<Arpanet:SAIL> MINIMA.[S77,JMC].            ↓ π∞↓↓ π>of FOL Proofs (to be published).

↓ ↓N↓↓αMcCarthy, J.↓ (1977b) First Order Theories of
↓ ↓N↓↓ ↓}Individual Concepts (to be published).
↓ ↓N↓↓ ↓}Available as <Arpanet:SAIL>
↓ ↓N↓↓ ↓}CONCEP.[E76,JMC].

↓ ↓N↓↓αMcCarthy, J.↓ (1977c) Ascribing Mental
↓ ↓N↓↓ ↓}Qualities to Machines (to be published).